Left Termination of the query pattern at_in_2(a, a) w.r.t. the given Prolog program could successfully be proven:



↳ Prolog
  ↳ PrologToPiTRSProof

Clauses:

at(X, fido) :- ','(at(X, mary), near(X)).
at(ta, mary).
at(jm, mary).
near(jm).

Queries:

at(a,a).

We use the technique of [30].Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

at_in(jm, mary) → at_out(jm, mary)
at_in(ta, mary) → at_out(ta, mary)
at_in(X, fido) → U1(X, at_in(X, mary))
U1(X, at_out(X, mary)) → U2(X, near_in(X))
near_in(jm) → near_out(jm)
U2(X, near_out(X)) → at_out(X, fido)

The argument filtering Pi contains the following mapping:
at_in(x1, x2)  =  at_in
jm  =  jm
mary  =  mary
at_out(x1, x2)  =  at_out(x1, x2)
ta  =  ta
fido  =  fido
U1(x1, x2)  =  U1(x2)
U2(x1, x2)  =  U2(x1, x2)
near_in(x1)  =  near_in(x1)
near_out(x1)  =  near_out

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog



↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof

Pi-finite rewrite system:
The TRS R consists of the following rules:

at_in(jm, mary) → at_out(jm, mary)
at_in(ta, mary) → at_out(ta, mary)
at_in(X, fido) → U1(X, at_in(X, mary))
U1(X, at_out(X, mary)) → U2(X, near_in(X))
near_in(jm) → near_out(jm)
U2(X, near_out(X)) → at_out(X, fido)

The argument filtering Pi contains the following mapping:
at_in(x1, x2)  =  at_in
jm  =  jm
mary  =  mary
at_out(x1, x2)  =  at_out(x1, x2)
ta  =  ta
fido  =  fido
U1(x1, x2)  =  U1(x2)
U2(x1, x2)  =  U2(x1, x2)
near_in(x1)  =  near_in(x1)
near_out(x1)  =  near_out


Using Dependency Pairs [1,30] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

AT_IN(X, fido) → U11(X, at_in(X, mary))
AT_IN(X, fido) → AT_IN(X, mary)
U11(X, at_out(X, mary)) → U21(X, near_in(X))
U11(X, at_out(X, mary)) → NEAR_IN(X)

The TRS R consists of the following rules:

at_in(jm, mary) → at_out(jm, mary)
at_in(ta, mary) → at_out(ta, mary)
at_in(X, fido) → U1(X, at_in(X, mary))
U1(X, at_out(X, mary)) → U2(X, near_in(X))
near_in(jm) → near_out(jm)
U2(X, near_out(X)) → at_out(X, fido)

The argument filtering Pi contains the following mapping:
at_in(x1, x2)  =  at_in
jm  =  jm
mary  =  mary
at_out(x1, x2)  =  at_out(x1, x2)
ta  =  ta
fido  =  fido
U1(x1, x2)  =  U1(x2)
U2(x1, x2)  =  U2(x1, x2)
near_in(x1)  =  near_in(x1)
near_out(x1)  =  near_out
AT_IN(x1, x2)  =  AT_IN
U11(x1, x2)  =  U11(x2)
U21(x1, x2)  =  U21(x1, x2)
NEAR_IN(x1)  =  NEAR_IN(x1)

We have to consider all (P,R,Pi)-chains

↳ Prolog
  ↳ PrologToPiTRSProof
    ↳ PiTRS
      ↳ DependencyPairsProof
        ↳ PiDP
          ↳ DependencyGraphProof

Pi DP problem:
The TRS P consists of the following rules:

AT_IN(X, fido) → U11(X, at_in(X, mary))
AT_IN(X, fido) → AT_IN(X, mary)
U11(X, at_out(X, mary)) → U21(X, near_in(X))
U11(X, at_out(X, mary)) → NEAR_IN(X)

The TRS R consists of the following rules:

at_in(jm, mary) → at_out(jm, mary)
at_in(ta, mary) → at_out(ta, mary)
at_in(X, fido) → U1(X, at_in(X, mary))
U1(X, at_out(X, mary)) → U2(X, near_in(X))
near_in(jm) → near_out(jm)
U2(X, near_out(X)) → at_out(X, fido)

The argument filtering Pi contains the following mapping:
at_in(x1, x2)  =  at_in
jm  =  jm
mary  =  mary
at_out(x1, x2)  =  at_out(x1, x2)
ta  =  ta
fido  =  fido
U1(x1, x2)  =  U1(x2)
U2(x1, x2)  =  U2(x1, x2)
near_in(x1)  =  near_in(x1)
near_out(x1)  =  near_out
AT_IN(x1, x2)  =  AT_IN
U11(x1, x2)  =  U11(x2)
U21(x1, x2)  =  U21(x1, x2)
NEAR_IN(x1)  =  NEAR_IN(x1)

We have to consider all (P,R,Pi)-chains
The approximation of the Dependency Graph [30] contains 0 SCCs with 4 less nodes.